(set-logic HO_ALL)
(set-info :status sat)
(set-option :produce-models true)
(declare-fun x () (Nullable Int))
(declare-fun y () (Nullable Int))
(declare-fun z () (Nullable Int))
(assert (distinct z (as nullable.null (Nullable Int))))
(assert (= z ((_ nullable.lift +) x y)))
(check-sat)
